\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{B}$).
\\[0ex]$\exists$\=$X$:AbsInterface(E)\+
\\[0ex]($\forall$$e$:E.
\\[0ex](($\uparrow$($e$ $\in_{b}$ $X$)) $\Leftarrow\!\Rightarrow$ ($\exists$$a$:E. (es{-}p{-}local{-}pred(${\it es}$;$\lambda$$e$.$\uparrow$($P$($e$)))($e$,$a$))))
\\[0ex]\& (($\uparrow$($e$ $\in_{b}$ $X$)) $\Rightarrow$ (es{-}p{-}local{-}pred(${\it es}$;$\lambda$$e$.$\uparrow$($P$($e$)))($e$,$X$($e$)))))
\-
\end{tabbing}